The pursuit of responsible AI raises the ante on both the trustworthy computing and formal methods communities.

This refinement process may necessitate modifying D, M, and/or P. - How does the specification of unseen data relate to the specification of the data on which M was trained and tested? In traditional verification, we aim to prove property, P, a universally quantified statement: for example, for all input values of integer variable x, the program will return a positive integer; or for all execution sequences x, the system will not deadlock. So the first question for proving P of an ML model, M, is: in P, what do we quantify over? For an ML model that is to be deployed in the real world, one reasonable answer is to quantify over data distributions. But a ML model is meant to work only for certain distributions that are formed by real world phenomena, and not for arbitrary distributions. We do not want to prove a property for all data distributions. This insight on the difference in what we quantify over and what the data represents for proving a trust property for M leads to novel specification questions: - How can we specify the class of distributions over which P should hold for a given M? Consider robustness and fairness as two examples: